'Weak Dependency Graph [60.0]' ------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { D(t()) -> 1() , D(constant()) -> 0() , D(+(x, y)) -> +(D(x), D(y)) , D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))) , D(-(x, y)) -> -(D(x), D(y))} Details: We have computed the following set of weak (innermost) dependency pairs: { D^#(t()) -> c_0() , D^#(constant()) -> c_1() , D^#(+(x, y)) -> c_2(D^#(x), D^#(y)) , D^#(*(x, y)) -> c_3(D^#(x), D^#(y)) , D^#(-(x, y)) -> c_4(D^#(x), D^#(y))} The usable rules are: {} The estimated dependency graph contains the following edges: {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))} ==> {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))} {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))} ==> {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))} ==> {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))} {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))} ==> {D^#(constant()) -> c_1()} {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))} ==> {D^#(t()) -> c_0()} {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} ==> {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))} {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} ==> {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} ==> {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))} {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} ==> {D^#(constant()) -> c_1()} {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} ==> {D^#(t()) -> c_0()} {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))} ==> {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))} {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))} ==> {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))} ==> {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))} {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))} ==> {D^#(constant()) -> c_1()} {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))} ==> {D^#(t()) -> c_0()} We consider the following path(s): 1) { D^#(+(x, y)) -> c_2(D^#(x), D^#(y)) , D^#(-(x, y)) -> c_4(D^#(x), D^#(y)) , D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: D(x1) = [0] x1 + [0] t() = [0] 1() = [0] constant() = [0] 0() = [0] +(x1, x2) = [0] x1 + [0] x2 + [0] *(x1, x2) = [0] x1 + [0] x2 + [0] -(x1, x2) = [0] x1 + [0] x2 + [0] D^#(x1) = [0] x1 + [0] c_0() = [0] c_1() = [0] c_2(x1, x2) = [0] x1 + [0] x2 + [0] c_3(x1, x2) = [0] x1 + [0] x2 + [0] c_4(x1, x2) = [0] x1 + [0] x2 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: { D^#(+(x, y)) -> c_2(D^#(x), D^#(y)) , D^#(-(x, y)) -> c_4(D^#(x), D^#(y)) , D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} Weak Rules: {} Details: We apply the weight gap principle, strictly orienting the rules {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} Details: Interpretation Functions: D(x1) = [0] x1 + [0] t() = [0] 1() = [0] constant() = [0] 0() = [0] +(x1, x2) = [1] x1 + [1] x2 + [0] *(x1, x2) = [1] x1 + [1] x2 + [4] -(x1, x2) = [1] x1 + [1] x2 + [0] D^#(x1) = [1] x1 + [1] c_0() = [0] c_1() = [0] c_2(x1, x2) = [1] x1 + [1] x2 + [1] c_3(x1, x2) = [1] x1 + [1] x2 + [1] c_4(x1, x2) = [1] x1 + [1] x2 + [1] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))} and weakly orienting the rules {D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {D^#(-(x, y)) -> c_4(D^#(x), D^#(y))} Details: Interpretation Functions: D(x1) = [0] x1 + [0] t() = [0] 1() = [0] constant() = [0] 0() = [0] +(x1, x2) = [1] x1 + [1] x2 + [0] *(x1, x2) = [1] x1 + [1] x2 + [8] -(x1, x2) = [1] x1 + [1] x2 + [8] D^#(x1) = [1] x1 + [1] c_0() = [0] c_1() = [0] c_2(x1, x2) = [1] x1 + [1] x2 + [1] c_3(x1, x2) = [1] x1 + [1] x2 + [7] c_4(x1, x2) = [1] x1 + [1] x2 + [1] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))} and weakly orienting the rules { D^#(-(x, y)) -> c_4(D^#(x), D^#(y)) , D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {D^#(+(x, y)) -> c_2(D^#(x), D^#(y))} Details: Interpretation Functions: D(x1) = [0] x1 + [0] t() = [0] 1() = [0] constant() = [0] 0() = [0] +(x1, x2) = [1] x1 + [1] x2 + [8] *(x1, x2) = [1] x1 + [1] x2 + [9] -(x1, x2) = [1] x1 + [1] x2 + [8] D^#(x1) = [1] x1 + [1] c_0() = [0] c_1() = [0] c_2(x1, x2) = [1] x1 + [1] x2 + [1] c_3(x1, x2) = [1] x1 + [1] x2 + [1] c_4(x1, x2) = [1] x1 + [1] x2 + [1] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { D^#(+(x, y)) -> c_2(D^#(x), D^#(y)) , D^#(-(x, y)) -> c_4(D^#(x), D^#(y)) , D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} Details: The given problem does not contain any strict rules 2) { D^#(+(x, y)) -> c_2(D^#(x), D^#(y)) , D^#(-(x, y)) -> c_4(D^#(x), D^#(y)) , D^#(*(x, y)) -> c_3(D^#(x), D^#(y)) , D^#(constant()) -> c_1()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: D(x1) = [0] x1 + [0] t() = [0] 1() = [0] constant() = [0] 0() = [0] +(x1, x2) = [0] x1 + [0] x2 + [0] *(x1, x2) = [0] x1 + [0] x2 + [0] -(x1, x2) = [0] x1 + [0] x2 + [0] D^#(x1) = [0] x1 + [0] c_0() = [0] c_1() = [0] c_2(x1, x2) = [0] x1 + [0] x2 + [0] c_3(x1, x2) = [0] x1 + [0] x2 + [0] c_4(x1, x2) = [0] x1 + [0] x2 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {D^#(constant()) -> c_1()} Weak Rules: { D^#(+(x, y)) -> c_2(D^#(x), D^#(y)) , D^#(-(x, y)) -> c_4(D^#(x), D^#(y)) , D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} Details: We apply the weight gap principle, strictly orienting the rules {D^#(constant()) -> c_1()} and weakly orienting the rules { D^#(+(x, y)) -> c_2(D^#(x), D^#(y)) , D^#(-(x, y)) -> c_4(D^#(x), D^#(y)) , D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {D^#(constant()) -> c_1()} Details: Interpretation Functions: D(x1) = [0] x1 + [0] t() = [0] 1() = [0] constant() = [0] 0() = [0] +(x1, x2) = [1] x1 + [1] x2 + [8] *(x1, x2) = [1] x1 + [1] x2 + [2] -(x1, x2) = [1] x1 + [1] x2 + [8] D^#(x1) = [1] x1 + [1] c_0() = [0] c_1() = [0] c_2(x1, x2) = [1] x1 + [1] x2 + [3] c_3(x1, x2) = [1] x1 + [1] x2 + [1] c_4(x1, x2) = [1] x1 + [1] x2 + [1] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { D^#(constant()) -> c_1() , D^#(+(x, y)) -> c_2(D^#(x), D^#(y)) , D^#(-(x, y)) -> c_4(D^#(x), D^#(y)) , D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} Details: The given problem does not contain any strict rules 3) { D^#(+(x, y)) -> c_2(D^#(x), D^#(y)) , D^#(-(x, y)) -> c_4(D^#(x), D^#(y)) , D^#(*(x, y)) -> c_3(D^#(x), D^#(y)) , D^#(t()) -> c_0()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: D(x1) = [0] x1 + [0] t() = [0] 1() = [0] constant() = [0] 0() = [0] +(x1, x2) = [0] x1 + [0] x2 + [0] *(x1, x2) = [0] x1 + [0] x2 + [0] -(x1, x2) = [0] x1 + [0] x2 + [0] D^#(x1) = [0] x1 + [0] c_0() = [0] c_1() = [0] c_2(x1, x2) = [0] x1 + [0] x2 + [0] c_3(x1, x2) = [0] x1 + [0] x2 + [0] c_4(x1, x2) = [0] x1 + [0] x2 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {D^#(t()) -> c_0()} Weak Rules: { D^#(+(x, y)) -> c_2(D^#(x), D^#(y)) , D^#(-(x, y)) -> c_4(D^#(x), D^#(y)) , D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} Details: We apply the weight gap principle, strictly orienting the rules {D^#(t()) -> c_0()} and weakly orienting the rules { D^#(+(x, y)) -> c_2(D^#(x), D^#(y)) , D^#(-(x, y)) -> c_4(D^#(x), D^#(y)) , D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {D^#(t()) -> c_0()} Details: Interpretation Functions: D(x1) = [0] x1 + [0] t() = [0] 1() = [0] constant() = [0] 0() = [0] +(x1, x2) = [1] x1 + [1] x2 + [8] *(x1, x2) = [1] x1 + [1] x2 + [2] -(x1, x2) = [1] x1 + [1] x2 + [8] D^#(x1) = [1] x1 + [1] c_0() = [0] c_1() = [0] c_2(x1, x2) = [1] x1 + [1] x2 + [3] c_3(x1, x2) = [1] x1 + [1] x2 + [1] c_4(x1, x2) = [1] x1 + [1] x2 + [1] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { D^#(t()) -> c_0() , D^#(+(x, y)) -> c_2(D^#(x), D^#(y)) , D^#(-(x, y)) -> c_4(D^#(x), D^#(y)) , D^#(*(x, y)) -> c_3(D^#(x), D^#(y))} Details: The given problem does not contain any strict rules